|
__NOTOC__ The QED manifesto was a proposal for a computer-based database of all mathematical knowledge, strictly formalized and with all proofs having been checked automatically. (Q.E.D. means ラテン語:''quod erat demonstrandum'' in Latin, meaning "which had to be demonstrated.") The idea for the project arose in 1993, mainly under the impetus of Robert Boyer. The goals of the project, tentatively named ''QED project'' or ''project QED'', were outlined in the QED manifesto, a document first published in 1994, with input from several researchers.〔(The QED Manifesto ) in ''Automated Deduction - CADE 12'', Springer-Verlag, Lecture Notes in Artificial Intelligence, Vol. 814, pp. 238-251, 1994. (HTML version )〕 Explicit authorship was deliberately avoided. A dedicated mailing list was created, and two scientific conferences on QED took place, the first one in 1994 at Argonne National Laboratories and the second in 1995 in Warsaw organized by the Mizar group.〔(The QED Workshop II report )〕 The project seems to have died in 1996, never having produced more than discussions and plans. In a 2007 paper, Freek Wiedijk identifies two reasons for the failure of the project.〔Freek Wiedijk, (The QED Manifesto Revisited ), 2007〕 In order of importance: * Very few people are working on formalization of mathematics. There is no compelling application for fully mechanized mathematics. * Formalized mathematics does not yet resemble real, traditional mathematics. This is partly due to the complexity of mathematical notation, and partly to the limitations of existing theorem provers and proof assistants; the paper finds that the major contenders, Mizar, HOL, and Coq, have serious shortcomings in their abilities to express mathematics. Nonetheless, QED-style projects are regularly proposed, and the Mizar library has successfully formalized a large portion of undergraduate mathematics. it is the largest such library.〔Fairouz Kamareddine, Manuel Maarek, Krzysztof Retel, and J. B. Wells, ''(Gradual Computerisation/Formalisation of Mathematical Texts into Mizar )''〕 Another such project is Metamath proof database. In 2014 the Twenty years of the QED Manifesto〔Twenty years of the QED Manifesto workshop ()〕 workshop was organized as part of the Vienna Summer of Logic. ==See also== * Formalism (mathematics) * Mathematical knowledge management * POPLmark, a more modest project in programming language theory 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「QED manifesto」の詳細全文を読む スポンサード リンク
|